#include "balance.h"

static const uint8_t sign_pos = 0x01;
static const uint8_t sign_neg = 0x02;
static const uint8_t sign_bi  = 0x03;
static const uint8_t sign_int = 0x04;

Balance::Balance()
{
}
bool Balance::collectAND( unsigned n , vec<AigLit> & fanin )
{
   unsigned * focnt = _focnt.data ;
   uint8_t  * polar = _polar.data;

   unsigned   ptr = 0;
   bool  isConst = false ;
   
   _tmp_cone.clear();
   _tmp_cone.push( n );

   do
   {
      n = _tmp_cone[ ptr ++ ];
      polar[n] |= sign_int;
      for( int i = 0 ; i < 2 ; ++i )
      {
         AigLit   p = eqIn( n , i );
         unsigned v = var( p );
         focnt[v] -=1;
         polar[v] |= sign(p)?sign_neg:sign_pos;
         if( focnt[v] == 0 && (polar[v] & sign_pos) )_tmp_cone.push(v);
      }
   }while( _tmp_cone.size() != ptr );

   for( unsigned i = 0 ; i < _tmp_cone.size() ;++i )
   {
      for( int j = 0 ; j < 2 ; ++ j )
      {
         AigLit p = eqIn( _tmp_cone[i] , j ) ;
         unsigned v = var(p);
         if( (polar[v] & sign_int) == 0 ) 
         {
            fanin.push(p);
            polar[v] |= sign_int;
         }
         if( (polar[v] & sign_bi )== sign_bi || p == 0) isConst = true;
      }//set polar[_tmp_cone[i]] = 0;
   }

   for( unsigned i=0;i< fanin.size();++i)
      polar[var(fanin[i])]=0;
   return isConst;
}
void Balance::run( unsigned t , vec<AigLit> & fanin)
{
   if( _focnt[t] == 0 ) return;
   if( todo( t )==false)return;
   fanin.clear();
   unsigned p ;
   unsigned outcnt=0;

   std::swap( _focnt[t] , outcnt);
   if( collectAND( t,fanin) ) p = 0 ;
   else p = var( build_blAND( fanin.data , fanin.size() ) );

   resume( _tmp_cone.data , _tmp_cone.sz );
   if( t != p )replace( t , p , outcnt);
   else        _focnt[t] += outcnt;
}
void Balance::init()
{
   _tmp_cone.growTo( 100 );
   _polar.growTo(sz,0);
   CktInfo::init();
}
void Balance::run()
{
   unsigned size = sz;
   vec<AigLit> v(100);

   for( unsigned i = size-1 ; i > _andFlag ; -- i)  
      if( (_polar[i] & sign_int ) == 0 )
         run(i,v);
}

